\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Qa}$, ${\it Rb}$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$), $f$:(E(${\it Ia}$)$\rightarrow$$B$),\+
\\[0ex]$g$:(E(${\it Ib}$)$\rightarrow$E).
\-\\[0ex]$g$ glues ${\it Ia}$:${\it Qa}$ $--$$f$$\rightarrow$ ${\it Ib}$:${\it Rb}$ $\Rightarrow$ ($g$ $\in$ E(${\it Ib}$)$\rightarrow$E(${\it Ia}$))
\end{tabbing}